$\forall$${\it xm}$:XM, $T$:Type, $P$:($T$$\rightarrow$Prop). ($\exists$$a$:$T$. $P$($a$)) $\Rightarrow$ ($\in$$x$:$T$. $P$($x$)) $\in$ $T$